Termination w.r.t. Q proof of /tmp/tmpEqJYkP/Ex5_DLMMU04

Termination w.r.t. Q of the following Term Rewriting System could be disproven:

Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

tail(cons(X, XS)) → activate(XS)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(activate(x₁)) = x₁
POL(cons(x₁, x₂)) = x₁ + x₂
POL(incr(x₁)) = x₁
POL(n__cons(x₁, x₂)) = x₁ + x₂
POL(n__incr(x₁)) = x₁
POL(n__repItems(x₁)) = 2·x₁
POL(n__take(x₁, x₂)) = x₁ + x₂
POL(n__zip(x₁, x₂)) = 2·x₁ + 2·x₂
POL(nil) = 0
POL(oddNs) = 0
POL(pair(x₁, x₂)) = 2·x₁ + x₂
POL(pairNs) = 0
POL(repItems(x₁)) = 2·x₁
POL(s(x₁)) = x₁
POL(tail(x₁)) = 1 + 2·x₁
POL(take(x₁, x₂)) = x₁ + x₂
POL(zip(x₁, x₂)) = 2·x₁ + 2·x₂

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

repItems(nil) → nil

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(activate(x₁)) = x₁
POL(cons(x₁, x₂)) = 2·x₁ + x₂
POL(incr(x₁)) = x₁
POL(n__cons(x₁, x₂)) = 2·x₁ + x₂
POL(n__incr(x₁)) = x₁
POL(n__repItems(x₁)) = 1 + 2·x₁
POL(n__take(x₁, x₂)) = x₁ + 2·x₂
POL(n__zip(x₁, x₂)) = 2·x₁ + 2·x₂
POL(nil) = 0
POL(oddNs) = 1
POL(pair(x₁, x₂)) = x₁ + 2·x₂
POL(pairNs) = 1
POL(repItems(x₁)) = 1 + 2·x₁
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = x₁ + 2·x₂
POL(zip(x₁, x₂)) = 2·x₁ + 2·x₂

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

zip(nil, XS) → nil
zip(X, nil) → nil
zip(X1, X2) → n__zip(X1, X2)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(activate(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(incr(x₁)) = 2·x₁
POL(n__cons(x₁, x₂)) = x₁ + x₂
POL(n__incr(x₁)) = x₁
POL(n__repItems(x₁)) = x₁
POL(n__take(x₁, x₂)) = x₁ + x₂
POL(n__zip(x₁, x₂)) = 1 + x₁ + x₂
POL(nil) = 0
POL(oddNs) = 0
POL(pair(x₁, x₂)) = x₁ + x₂
POL(pairNs) = 0
POL(repItems(x₁)) = 2·x₁
POL(s(x₁)) = 2·x₁
POL(take(x₁, x₂)) = 2·x₁ + 2·x₂
POL(zip(x₁, x₂)) = 2 + 2·x₁ + 2·x₂

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

take(0, XS) → nil

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(activate(x₁)) = x₁
POL(cons(x₁, x₂)) = x₁ + x₂
POL(incr(x₁)) = x₁
POL(n__cons(x₁, x₂)) = x₁ + x₂
POL(n__incr(x₁)) = x₁
POL(n__repItems(x₁)) = 2·x₁
POL(n__take(x₁, x₂)) = 1 + x₁ + x₂
POL(n__zip(x₁, x₂)) = x₁ + 2·x₂
POL(nil) = 0
POL(oddNs) = 0
POL(pair(x₁, x₂)) = x₁ + x₂
POL(pairNs) = 0
POL(repItems(x₁)) = 2·x₁
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + x₁ + x₂
POL(zip(x₁, x₂)) = x₁ + 2·x₂

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

take(X1, X2) → n__take(X1, X2)
repItems(X) → n__repItems(X)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(activate(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(incr(x₁)) = 2·x₁
POL(n__cons(x₁, x₂)) = x₁ + x₂
POL(n__incr(x₁)) = x₁
POL(n__repItems(x₁)) = 1 + x₁
POL(n__take(x₁, x₂)) = 1 + x₁ + x₂
POL(n__zip(x₁, x₂)) = x₁ + x₂
POL(oddNs) = 0
POL(pair(x₁, x₂)) = 2·x₁ + 2·x₂
POL(pairNs) = 0
POL(repItems(x₁)) = 2 + 2·x₁
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(zip(x₁, x₂)) = 2·x₁ + 2·x₂

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
activate(n__take(X1, X2)) → take(X1, X2)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(activate(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 2·x₁ + x₂
POL(incr(x₁)) = 2·x₁
POL(n__cons(x₁, x₂)) = x₁ + x₂
POL(n__incr(x₁)) = x₁
POL(n__repItems(x₁)) = 1 + x₁
POL(n__take(x₁, x₂)) = 1 + x₁ + x₂
POL(n__zip(x₁, x₂)) = 1 + x₁ + x₂
POL(oddNs) = 0
POL(pair(x₁, x₂)) = 2·x₁ + x₂
POL(pairNs) = 0
POL(repItems(x₁)) = 2 + 2·x₁
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(zip(x₁, x₂)) = 2 + 2·x₁ + 2·x₂

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

activate(n__repItems(X)) → repItems(X)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(activate(x₁)) = x₁
POL(cons(x₁, x₂)) = x₁ + x₂
POL(incr(x₁)) = x₁
POL(n__cons(x₁, x₂)) = x₁ + x₂
POL(n__incr(x₁)) = x₁
POL(n__repItems(x₁)) = 2 + x₁
POL(n__take(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(n__zip(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(oddNs) = 0
POL(pairNs) = 0
POL(repItems(x₁)) = 1 + x₁
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(zip(x₁, x₂)) = 2 + x₁ + x₂

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
activate(n__zip(X1, X2)) → zip(X1, X2)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(activate(x₁)) = x₁
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(incr(x₁)) = 2·x₁
POL(n__cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(n__incr(x₁)) = 2·x₁
POL(n__take(x₁, x₂)) = x₁ + x₂
POL(n__zip(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(oddNs) = 0
POL(pairNs) = 0
POL(s(x₁)) = 2·x₁
POL(take(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(zip(x₁, x₂)) = x₁ + x₂

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

                                ↳ QTRS

                                  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

INCR(cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__incr(X)) → INCR(X)
PAIRNS → ODDNS
ODDNS → PAIRNS
PAIRNS → CONS(0, n__incr(oddNs))
ACTIVATE(n__cons(X1, X2)) → CONS(X1, X2)
INCR(cons(X, XS)) → CONS(s(X), n__incr(activate(XS)))
ODDNS → INCR(pairNs)

The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

INCR(cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__incr(X)) → INCR(X)
PAIRNS → ODDNS
ODDNS → PAIRNS
PAIRNS → CONS(0, n__incr(oddNs))
ACTIVATE(n__cons(X1, X2)) → CONS(X1, X2)
INCR(cons(X, XS)) → CONS(s(X), n__incr(activate(XS)))
ODDNS → INCR(pairNs)

The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 4 less nodes.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

INCR(cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__incr(X)) → INCR(X)

The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QDPSizeChangeProof

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

INCR(cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__incr(X)) → INCR(X)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ACTIVATE(n__incr(X)) → INCR(X)
The graph contains the following edges 1 > 1
INCR(cons(X, XS)) → ACTIVATE(XS)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

PAIRNS → ODDNS
ODDNS → PAIRNS

The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

PAIRNS → ODDNS
ODDNS → PAIRNS

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

PAIRNS → ODDNS
ODDNS → PAIRNS

The TRS R consists of the following rules:none

s = ODDNS evaluates to t =ODDNS

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

ODDNS → PAIRNS
with rule ODDNS → PAIRNS at position [] and matcher [ ]

PAIRNS → ODDNS
with rule PAIRNS → ODDNS

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.